include "arithmetics/nat.ma".
include "basics/deqsets.ma". 
include "basics/lists/list.ma".
include "basics/lists/listb.ma".


(********************************************)
(********** ATOMI *************)
inductive Atom: Type[0] ≝
   Name  : nat → Atom
 | CoName: nat → Atom .

(* Atom: notation and interpretation *)
interpretation "Name" 'Name n = (Name n).
notation "hvbox(𝔸 \sub n)" with precedence 90 for @{ 'Name $n }.

(* Negative atom: notation and interpretation *)
notation "hvbox(𝔹 \sub n)" with precedence 90 for @{ 'CoName $n }.
interpretation "CoName" 'CoName n = (CoName n).

(* Per definire insiemi di nomi e co-nomi tramite funzione caratteristica
come nel seguente esempio:
definition exSetB ≝ { 𝔸 \sub 2 } ∪ {𝔹 \sub 2} .
occorre avere 'include "basics/sets.ma"' .
Non seguirò questa strada perché mi pare servano strutture in cui cercare 
effettivamente gli atomi. Ovvero servono liste su insiemi con equivalenza
decidibile, come indicato da chapter5.ma e chapter6.ma. *)

definition Atomeqb ≝ λa,b:Atom.
  match a with 
  [ Name   n ⇒ match b with [ Name   m ⇒ (eqb n m)
                              | _        ⇒ false]
  | CoName n ⇒ match b with [ CoName m ⇒ (eqb n m)
                              | _        ⇒ false]].
               
notation < "a == b" non associative 
      with precedence 45 for @{Atomeqb $a $b }.

lemma Atomeqb_true: ∀a,b. iff (Atomeqb a b = true) (a = b).
(* Ho guardato la dimostrazione del lemma 
   beqitem_true in chapter7.ma del tutorial ed ho
   provato a non saltare neanche un passo. *)
#a elim a -a
#X #b cases b -b
#Y %
[1,3,5,7: #H normalize in H; destruct 
          (* applico theorem eqb_true_to_eq: 
                        ∀n,m:nat. eqb n m = true → n = m.
             in rithmetics/nat.ma *)
          lapply (eqb_true_to_eq X Y H) -H
          #Heq <Heq @refl
|2,4,6,8: #H normalize destruct
         (* applico theorem eqb_n_n: ∀n. eqb n n = true.
            in rithmetics/nat.ma *)
          @(eqb_n_n Y)
] qed .

(* Grazie al lemma precedente ho che gli Atomi formano un insieme
con equivalenza decidibile. *)
definition AtomDeqSet ≝ mk_DeqSet Atom Atomeqb Atomeqb_true.

(* A me viene da dire che si dovrebbe poter dimostrare:
   lemma  Atomeqb_false: ∀a,b:AtomDeqSet. (eqb_false AtomDeqSet a b).
ma lo statement non piace a Matita. 
La sua 'forma esplosa' è qui sotto dimostrata semplicemente copiando 
la dimostrazione di:
   lemma eqb_false: ∀S:DeqSet.∀a,b:S. (eqb ? a b) = false ↔ a ≠ b.
in basics/deqsets.ma la quale è dimostrabile toglendo #S. *)
lemma Atomeqb_false: ∀a,b:AtomDeqSet. (eqb AtomDeqSet a b) = false ↔ a ≠ b.
#a #b % #H 
  [@(not_to_not … not_eq_true_false) #H1 <H @sym_eq @(\b H1)
  |cases (true_or_false (eqb ? a b)) // #H1 @False_ind @(absurd … (\P H1) H)
  ] qed.

(* Segue la decidibilità, anche questa copiata da basics/deqsets.ma 
ed adattata. *)
lemma Atomdec_eq: ∀a,b:AtomDeqSet. a = b ∨ a ≠ b.
#a #b cases (true_or_false (eqb ? a b)) #H
  [%1 @(\P H) | %2 @(\Pf H)] qed.

(* Prima di procedere nello sfruttare AtomDeqSet, definisco la negazione
su Atom, in modo da collegare ogni nome col suo co-nome. Immagino che poi
servirà... .*)
definition Atomneg ≝ λa:Atom.
  match a with 
  [ Name   n ⇒ CoName n
  | CoName n ⇒ Name   n  ].

lemma Atomneg_idem : ∀ a: Atom. Atomneg (Atomneg a) = a.
#a cases a #N normalize @refl qed .

(* Ho l'idea che:
   (par [𝔸_n,𝔹_m,𝔹_m,]) e (par [𝔹_m,𝔸_n,𝔹_m])   (1)
   (cop [𝔸_n,𝔹_m,𝔹_m]) e (cop [𝔹_m,𝔸_n,𝔹_m])   (2)
debbano essere in relazione di eguaglianza. Al contrario:
   (seq [𝔸_n,𝔹_m]) e (seq [𝔹_m,𝔸_n])   (3)
non lo devono essere. Ovvero vorrei sfruttare l'ordine implicito in
ogni lista per rappresentare la non commutatività del seq.

Sia (1) che (2) implicano la ncessità di poter vedere le liste di nomi e conomi
come multi-insiemi quando ad essi sia applicato uno tra par o cop.

Segue la relazione che dovrebbe permettere di assumere un tale punto di vista, 
ammesso che riusciamo a dimostrare che sia una relazione di equivalenza, o,
dopo aver definito le strutture, una congruenza. *)

inductive ListAsMultiSeteq  (A:Type[0]) : list A → list A → Prop ≝ 
  | lambaseeqbase : ∀l',t':list A. l'@t'=(nil A) → ListAsMultiSeteq A (nil A) (l'@t')
  | lambaseeqind : ∀h:A.∀t,l',t':list A.
                     t≠[ ] →  
                     ListAsMultiSeteq A t (append A l' t') → 
                        ListAsMultiSeteq A (cons A h t) 
                                           (append A (append A l' [h]) t')
.

lemma ListAsMultiSeteq_refl: 
∀A.∀l:list A. ListAsMultiSeteq A l l.
#A #l elim l 
[ @(lambaseeqbase A [ ] [ ]) normalize @refl 
| #h #t #Hind 
   @(lambaseeqind A h t [ ] t) normalize [ |@Hind ] 
  
] qed.

lemma xx: ∀A,h,t. Not (ListAsMultiSeteq A [ ] (cons A h t)).
#A #h #t @nmk #H @(absurd (ListAsMultiSeteq A [] (h::t))) 
[-H lapply (lambaseeqind A h [ ] [ ] t ) 
normalize
]


lemma ListAsMultiSeteq_symm: 
∀A.∀l,l':list A. ListAsMultiSeteq A l l' → ListAsMultiSeteq A l' l.
#A #l #l'  elim l elim l'
[ // 
| #h' #t' #Hind  

   ] 
]

inversion l' 
  [ #lempry @(lambaseeqbase A) 
  | #hl' #tl' #ltl -l'
  #lteq #lhteq destruct ]
| #h #t #Hind 
  @(lambaseeqind A h t [ ] t) normalize @Hind ] qed.




(* lemma ListAsMultiSeteq_tran: 
∀A.∀l,l',l'':list A. ListAsMultiSeteq A l l' → 
   ListAsMultiSeteq A l' l'' → ListAsMultiSeteq A l l'' . *)



(* Il prossimo passo è definire ListAsMultiDecSeteq il cui scopo è riflettere il
comportamento della generica relazione (di equivalenza??) ListaAsMultiSeteq 
in maniera decidibile. 
Il primo passo è scrivere filter_out_firstocc una versione di 
basics/lists/list.ma/filter che elimini da una lista la sola prima occorrenza di 
un elemento x in una data lista l. *) 
let rec filter_out_firstocc (A:DeqSet) (x:A) (l:list A) on l : list A ≝  
 match l with
 [ nil ⇒ (nil A)
 | cons h t ⇒ match (eqb A x h) with
              [ true  ⇒ t 
              | false ⇒ cons A h (filter_out_firstocc A x t)] ].

(* Ne consegue che ListAsMultiDecSeteq, date l e l', per ogni elemento h di l,
ne cerca la prima occorrenza in l'. Trovandola la cancella. Se il risultato è
svuotare contemporaneamente l ed l', esse conicidon a meno dell'ordine 
degli elementi. *)
let rec ListAsMultiDecSeteq  (A:DeqSet) (l:list A) (l':list A) on l: bool ≝ 
  match l with
  [ nil ⇒ match l' with [ nil ⇒ true | _   ⇒ false ]
  | cons h t ⇒ match l' with [ nil ⇒ false
                              | _   ⇒  ListAsMultiDecSeteq 
                                            A t (filter_out_firstocc A h l') ]].



(* Alcuni esempi di funzionamento di ListAsMultiDecSeteq:
lemma ListAsMultiDecSeteq_ex0:
ListAsMultiDecSeteq AtomDeqSet [] [] = true. normalize // qed .

lemma ListAsMultiDecSeteq_ex0':
ListAsMultiDecSeteq AtomDeqSet [] (𝔸 \sub 1)::[]) = false. normalize // qed .

lemma ListAsMultiDecSeteq_ex0'':
ListAsMultiDecSeteq AtomDeqSet ((𝔸 \sub 1)::[]) [] = false. normalize // qed .

lemma ListAsMultiDecSeteq_ex1:
ListAsMultiDecSeteq AtomDeqSet ((𝔸 \sub 1)::[])  ((𝔸 \sub 1)::[]) = true.
normalize // qed .

lemma ListAsMultiDecSeteq_ex2:
ListAsMultiDecSeteq AtomDeqSet ((𝔸 \sub 1)::[]) ((𝔸 \sub 1)::(𝔸 \sub 2)::[]) = false.
normalize // qed .

lemma ListAsMultiDecSeteq_ex3:
ListAsMultiDecSeteq AtomDeqSet ((𝔸 \sub 1)::(𝔸 \sub 2)::[]) 
                               ((𝔸 \sub 1)::(𝔸 \sub 2)::[]) = true. normalize // qed .

lemma ListAsMultiDecSeteq_ex4:
ListAsMultiDecSeteq AtomDeqSet ((𝔸 \sub 1)::(𝔸 \sub 2)::[]) 
                               ((𝔸 \sub 2)::(𝔸 \sub 1)::[]) = true. normalize // qed .

lemma ListAsMultiDecSeteq_ex5:
ListAsMultiDecSeteq AtomDeqSet ((𝔸 \sub 2)::(𝔸 \sub 1)::(𝔸 \sub 2)::[]) 
                               ((𝔸 \sub 1)::(𝔸 \sub 2)::(𝔸 \sub 2)::[]) = true.
normalize // qed .  --------------------------------------- *)

(* Il seguente  principio di induzione sul list DeqSet, che non mi pare essere
stato dipostrato può essere utile. 
lemma list_ind : ∀T:DeqSet.∀l:list T.∀P:list T → Prop.
  (P []) → (∀t,h. P t → P (h::t)) → P l.
#T #l #P #Pnil #Pcons elim l [@Pnil | -Pnil #H #T @Pcons ] qed. ----------*)


(* Manca almeno .. *)
lemma ListAtomeqb_true: 
 ∀a,b: list AtomDeqSet. iff (ListAsMultiDecSeteq AtomDeqSet a b = true) 
                            (ListAsMultiSeteq    AtomDeqSet  a b).
(* dimostrazione ancora da fare *)
               

(*****************************)
(******** OPERATORI **********)
inductive  Operator : Type[0] ≝
|  par : Operator
|  seq : Operator
|  cop : Operator .

definition Operatoreqb ≝ λa,b:Operator.
  match a with 
  [ par ⇒ match b with [ par ⇒ true | _ ⇒ false]
  | seq ⇒ match b with [ seq ⇒ true | _ ⇒ false]
  | cop ⇒ match b with [ cop ⇒ true | _ ⇒ false]].

lemma Operatoreqb_true: ∀a,b. 
   iff (Operatoreqb a b = true) (a = b).
#a cases a -a #b cases b -b %
[1,3,5,7,9,11,13,15,17: #H normalize in H; destruct @refl
|2,4,6,8,10,12,14,16,18: #H normalize destruct @refl
] qed .

definition OperatorDeqSet ≝ mk_DeqSet Operator Operatoreqb Operatoreqb_true.

lemma Operatoreqb_false: 
   ∀a,b:OperatorDeqSet. (eqb ? a b) = false ↔ a ≠ b.
#a #b % #H 
  [@(not_to_not … not_eq_true_false) #H1 <H @sym_eq  @(\b H1)
  |cases (true_or_false (eqb ? a b)) // #H1 @False_ind @(absurd … (\P H1) H)
  ] qed.

lemma Opeartordec_eq: ∀a,b:OperatorDeqSet. a = b ∨ a ≠ b.
#a #b cases (true_or_false (eqb ? a b)) #H
  [%1 @(\P H) | %2 @(\Pf H)] qed.

(*****************************)
(******** Strutture **********)
inductive Structure : Type[0] ≝
|  unit   : Structure
|  sbase  : Operator → list AtomDeqSet → Structure
|  sind   : Operator → list Structure  → Structure .

definition Structureqb ≝ λa,b:Structure.
  match a with 
  [ unit      ⇒ match b with 
                 [ unit ⇒ true | _    ⇒ false]
  | sbase o l ⇒ match b with 
                 [ sbase o' l' ⇒ (Operatoreqb o o') ∧ 
                                    (* Quella che segue deve essere 
                                    un po' sofisticata. *) 
                                    (ListAtomDeqSeteqb l l') 
                 | _           ⇒ false]
  | sind  o l ⇒ match b with 
                 [ sind o' l'  ⇒ (Operatoreqb o o') ∧ 
                                    (* Quella che segue deve essere 
                                     ancora più sofisticata della
                                     precedente. *) 
                                    (ListAtomDeqSeteqb l l')
                 | _           ⇒ false] ].
               
notation < "a == b" non associative with precedence 45 for @{Atomeqb $a $b }.

lemma Structureqb_true: ∀a,b. iff (Structureeqb a b = true) (a = b).
#a elim a -a
#X #b cases b -b
#Y %
[1,3,5,7: #H normalize in H; destruct 
          (* applico theorem eqb_true_to_eq: 
                        ∀n,m:nat. eqb n m = true → n = m.
             in rithmetics/nat.ma *)
          lapply (eqb_true_to_eq X Y H) -H
          #Heq <Heq @refl
|2,4,6,8: #H normalize destruct
         (* applico theorem eqb_n_n: ∀n. eqb n n = true.
            in rithmetics/nat.ma *)
          @(eqb_n_n Y)
] qed .

(* Grazie al lemma precedente ho che gli Atomi formano un insieme
con equivalenza decidibile. *)
definition AtomDeqSet ≝ mk_DeqSet Atom Atomeqb Atomeqb_true.

let rec Structureneg (s:Structure) on s : Structure ≝ 
match s with 
[ unit      ⇒ unit
| sbase o l ⇒ match o with
               [ par ⇒ (sbase cop (map ?? Atomneg l))
               | seq ⇒ (sbase seq (map ?? Atomneg l))
               | cop ⇒ (sbase par (map ?? Atomneg l))]
| sind o l  ⇒ match o with
              [ par ⇒ match l with 
                      [ nil      ⇒ sind cop []
                      | cons h t ⇒ sind cop 
                                        ((Structureneg h):: 
                                          (map ?? Structureneg t))]
              | seq ⇒ match l with 
                      [ nil      ⇒ sind seq []
                      | cons h t ⇒ sind seq 
                                        ((Structureneg h):: 
                                          (map ?? Structureneg t))]
              | cop ⇒ match l with 
                      [ nil      ⇒ sind par []
                      | cons h t ⇒ sind par 
                                        ((Structureneg h):: 
                                          (map ?? Structureneg t))]  
             ]
].


(* Il principio di induzione potrebbe essere tipo il seguente. *)
theorem Structure_induction: 
∀P:Structure → Prop. 
    P unit → 
    (∀o:Operator. P (sbase o [])) → 
    (∀o:Operator.∀l:list AtomDeqSet. P (sbase o l)) →
    (∀o:Operator. P (sind o [])) → 
    (∀o:Operator.∀h:Structure.∀t:list Structure. 
        P h → P (sind o t) → P (sind o (h::t))) → 
    (∀s:Structure. P s) .
(* da fare *)


(* check Structureneg. *)

(* Da dimostrare a pezzi sfruttando Structure_induction alla fine. *)
lemma Structureneg_idem: ∀s:Structure. Structureneg (Structureneg s) = s.
#s cases s 
[ normalize @refl ] (* Primo goal *)
#L elim L 
[1,3,5,7,9,11: normalize @eq_f @refl
|2,4,6: #Hh #Ht 
 cases Hh #N #Hind normalize
  @eq_f @eq_f  (* ??????? *)
 ]
]  qed .


definition Structureeqb ≝ λa,b:Atom.
notation < "a ≡ b" non associative with precedence 45 for @{Atomeqb $a $b }.

let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝ 
match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].



(**********************************************************)
(* Abbozzo di una possibile strada alternativa
per definire le strutture. *)
definition Atomword ≝ list AtomDeqSet.
definition AtomBag1 ≝ [ 𝔸 \sub 1; 𝔹 \sub 2 ].

(* Unit: notation and interpretation *)
interpretation "Unit" 'Unit = (nil AtomDeqSet).
notation "𝟙" non associative with precedence 90 for @{ 'Unit }.
(* check 𝟙. *)

(* Par *)
inductive Par (A,B:Prop) : Prop ≝
    mkPar : A → B → Par A B.
(* Seq *)
inductive Seq (A,B:Prop) : Prop ≝
    mkSeq : A → B → Seq A B.
(* CoP *)
inductive CoP (A,B:Prop) : Prop ≝
    mkCoP : A → B → CoP A B.

(**********************************************************)
(* Altro abbozzo di definizione alternativa per la definizione
delle strutture. *)
definition name   ≝ λA:Type[0].λx,a:A.〈 x=a, true 〉.
interpretation "name" 'name x = (name ? x).
notation "x+" with precedence 100 for @{name $x}.  
definition coname ≝ λA:Type[0].λx,a:A.〈 x=a, false 〉.
interpretation "singleton" 'coname x = (coname ? x).
notation "x-" with precedence 100 for @{coname $x}.

(* check name.   *)
definition a_a ≝ name nat 1. definition a_b ≝ name nat 2.
definition a_c ≝ name nat 3. definition a_d ≝ name nat 4.
definition ca_a ≝ coname nat 1. definition ca_b ≝ coname nat 2.
definition ca_c ≝ coname nat 3. definition ca_d ≝ coname nat 4.

inductive operator : Type[0] ≝
  mkpar : operator
| mkcopar : operator
| mkseq : operator.  